Search for: All records

Exact probabilistic inference is a requirement for many applications of probabilistic programming languages (PPLs) such as in high-consequence settings or verification. However, designing and implementing a PPL with scalable high-performance exact inference is difficult: exact inference engines, much like SAT solvers, are intricate low-level programs that are hard to implement. Due to this implementation challenge, PPLs that support scalable exact inference are restrictive and lack many features of general-purpose languages. This paper presents Roulette, the first discrete probabilistic programming language that combines high-performance exact inference with general-purpose language features. Roulette supports a significant subset of Racket, including data structures, first-class functions, surely-terminating recursion, mutable state, modules, and macros, along with probabilistic features such as finitely supported discrete random variables, conditioning, and top-level inference. The key insight is that there is a close connection between exact probabilistic inference and the symbolic evaluation strategy of Rosette. Building on this connection, Roulette generalizes and extends the Rosette solver-aided programming system to reason about probabilistic rather than symbolic quantities. We prove Roulette sound by generalizing a proof of correctness for Rosette to handle probabilities, and demonstrate its scalability and expressivity on a number of examples. 

Currently, there is a gap between the tools used by probability theorists and those used in formal reasoning about probabilistic programs. On the one hand, a probability theorist decomposes probabilistic state along the simple and natural product of probability spaces. On the other hand, recently developed probabilistic separation logics decompose state via relatively unfamiliar measure-theoretic constructions for computing unions of sigma-algebras and probability measures. We bridge the gap between these two perspectives by showing that these two methods of decomposition are equivalent up to a suitable equivalence of categories. Our main result is a probabilistic analog of the classic equivalence between the category of nominal sets and the Schanuel topos. Through this equivalence, we validate design decisions in prior work on probabilistic separation logic and create new connections to nominal-set-like models of probability. 

Soft robotics has yielded numerous examples of soft grippers that utilize compliance to achieve impressive grasping performances with great simplicity, adaptability, and robustness. Designing soft grippers with substantial grasping strength while remaining compliant and gentle is one of the most important challenges in this field. In this paper, we present a light-weight, vacuum-driven soft robotic gripper made of an origami “magic-ball” and a flexible thin membrane. We also describe the design and fabrication method to rapidly manufacture the gripper with different combinations of low- cost materials for diverse applications. Grasping experiments demonstrate that our gripper can lift a large variety of objects, including delicate foods, heavy bottles, and other miscellaneous items. The grasp force on 3D-printed objects is also characterized through mechanical load tests. The results reveal that our soft gripper can produce significant grasp force on various shapes using negative pneumatic pressure (vacuum). This new gripper holds the potential for many practical applications that require safe, strong, and simple grasping.